COMMENT ⊗   VALID 00008 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002				PATHS AND REVERSING
C00004 00003	
C00006 00004		Proof of theorem (Version 1): Suppose such  a path P exists. 
C00009 00005	subtree of M1.  Let P1 be  a minimal length path in this set, and let
C00012 00006		It is not difficult to show that this bound is  tight.  It is
C00014 00007		Definition: Two  mate pairs x  and y of  a semantic  tree are
C00016 00008		Proof of lemma: By  applying lemma 2 above to  the reverse of
C00018 ENDMK
C⊗;
			PATHS AND REVERSING

	Now  we discuss  ways  in  which a  path  of mate  pairs  can
"reverse" or  "repeat" itself.  Also, we  discuss properties of paths
that do not reverse themselves. 

	Definition: Two  mate  pairs (L1  , M1)  and  (L2 ,  M2)  are
πreversing if L1 and M2 are identical and if M1 and L2 are identical. 
We also say that (L1 , M1) πreverses (L2 , M2) in such a case. 

	Definition:  Two mate  pairs (L1  , M1)  and (L2  , M2)  of a
semantic tree T are  πarc πreversing if L1  and M2 occur at  the same
arc (and if M1 and L2 occur at the same arc).  We also say that (L1 ,
M1) πarc πreverses (L2 , M2) in such a case. 

	Definition: A path  of mate  pairs in  a semantic  tree T  is
πreversing if  two elements  of the path  are reversing.   A path  is
πnon-πreversing if it  is not reversing.  Note that it is possible to
have infinite  non-reversing  continuous paths  of  mate pairs  in  a
finite semantic tree. 

	Definition: A  path of mate  pairs is πarc πreversing  if two
elements  of  the  path  are arc  reversing.    A  path  is πnon-πarc
πreversing if it is not arc reversing. 

	Definition: The πsubtree πof a distinguished literal L is the
subtree of the son node of the arc at which L occurs. 

	Theorem  (No Infinite Non-Arc  Reversing Paths): There  is no
infinite continuous non-arc reversing path of mate pairs in a  finite
semantic tree with variables. 

	Lemma 1 (Paths Exiting Subtrees):  Suppose mate pair (L1 , M1)
has an occurrence in a continuous path P of mate pairs.  Then one of
the following is true:

	a.)  All mate pairs in P after the occurrence of (L1 , M1)
are within the subtree of M1.  (Recall the above definition.)

	b.)  The first occurrence of a mate pair (L2 , M2) in P that
is not in the subtree of M1 and occurs after the occurrence of (L1 , M1)
either

	b1.)  is below (L1 , M1) or
	b2.)  arc reverses (L1 , M1).

	Proof:  The only way P can get out of the subtree of M1 is by
reversing (L1 , M1) or by going below it.  See figure 3.1.

	Proof of theorem (Version 1): Suppose such  a path P exists. 
Consider  the set of  nodes that occur  infinitely often  in the node
path PN of P.   Let N be a node which  is minimal in this set in  the
standard node ordering.   Choose some integer i such  that PN(i), the
i-th  element of PN,  is N and  such that for all  integers j greater
than i, PN(j) is not below N.  (Such an occurrence  of N must exist.)
Let j  be the least  integer greater than  i such that  the mate pair
P(j) has N as father node.  (Such a j must exist.) Then by the  above
lemma, P(j) arc reverses P(i).  Hence P is arc reversing.  See figure
3.3.

	For the second  version of the  proof, we need  the following
lemma:

	Lemma 2:  Suppose (L1 , M1) occurs in  a continuous path P of
mate pairs.  Then if P ever  enters the subtree of L1, there must  be
at least one  arc reversal in P  between the occurrence of  (L1 , M1)
and the  entry of the subtree of L1.  More precisely, the set of mate
pairs including (L1  , M1) and all  mate pairs occurring after  (L1 ,
M1) in P  but before the entry of the  subtree, must contain two mate
pairs that are arc reversing. 

	Proof of  Lemma  2:  Consider  the set  of  paths  which  are
counter-examples to lemma 2.  That is, there is a mate pair (L1 , M1)
in  the path and  a later entry  into the subtree  of L1,  but no arc
reversal between the  occurrence of (L1  , M1) and  the entry of  the
subtree of M1.  Let P1 be  a minimal length path in this set, and let
(L1 , M1)  be such a mate pair as above.  Note that (L1 , M1) will be
the first mate pair in  P1.  Consider the first occurrence of  a mate
pair x in P1  such that x is not (L1 , M1) and  such that x is not in
the subtree of M1.  Such an  occurrence must exist in P1, or else  P1
never leaves the subtree  of M1.  Let (L2  , M2) be the mate  pair x.
Then (L2 , M2) must  be below (L1 , M1) by lemma 1  since P1 can have
no arc reversal there.   Therefore (L1 , M1) is in the subtree of L2.
Hence in order to get into the  subtree of L1, P1 must also get  into
the  subtree of  L2.    Therefore the  portion  of  P1 including  the
occurrence of (L2 , M2) and all succeeding elements must be a shorter
path which is  also a counter-example to  lemma 2.  This  contradicts
the  assumption  that  P1 is  of  minimal  length  among the  set  of
counter-examples  to  lemma  2.     Hence  lemma   2  must  have   no
counter-examples.  See figure 3.2.

	Proof of Theorem (Version 2): No node  can occur twice in the
node  path of a non-arc  reversing continuous path P  of mate pairs.  
For if some node N occurred twice with no lower node in between, then
P would be arc  reversing by lemma 1.  If a lower  node M occurred in
between, then N would become inaccessible by lemma 2. 

	Corollary:  In  a  semantic tree  with  j  interior  nodes, a
non-arc reversing continuous path P can be of length at most j. 

	It is not difficult to show that this bound is  tight.  It is
easy to construct finite semantic trees T of arbitrary size and shape
such that a non-arc reversing continuous path in T exists whose  node
path  includes every  interior node  of  T.   Later  we will  discuss
sufficient conditions for such a path to exist in a semantic tree. 

	Definition: A path P of mate pairs  is πrepeating if there is
a mate pair that occurs two or more times in P. 

	Definition: Two  mate pairs (L1 , M1) and  (L2 , M2) are πarc
πrepeating if L1 and L2 occur at the same arc (and if M1 and M2 occur
at the same arc). 

	Definition: A  path P of mate  pairs in a semantic  tree T is
πarc  πrepeating if two elements  of P are arc repeating.   A path is
πnon-πarc πrepeating if no two elements are repeating.   Note that if
a continuous path  of mate pairs is non-arc  repeating, then its node
path includes each interior node of the tree at most twice.  Later we
will  discuss sufficient  conditions  for  the existence  of  non-arc
repeating  continuous paths whose  node path  includes every interior
node of the tree exactly twice. 

	Definition: Two  mate pairs x  and y of  a semantic  tree are
πdistinguished πclause πrepeating if there are distinguished literals
L1 and L2 of x  and y, respectively, such that  L1 and L2 are in  the
same distinguished clause. 

	Definition: A path  P of mate pairs  in a semantic tree  T is
πdistinguished πclause πrepeating if two non-adjacent mate pairs of P
are distinguished clause  repeating.  A  path is  πnon-πdistinguished
πclause πrepeating if it is not distinguished clause repeating.  Note
that  any  ascending  path  of  mate  pairs  which is  continuous  is
non-distinguished clause repeating.  We have the following result:

	Theorem   (Distinguished   Clause   Repeating   Implies   Arc
Reversing): If a continuous path P of mate pairs in a semantic tree T
is distinguished clause repeating, then it is arc reversing. 

	Lemma: Suppose mate  pair (L1  , M1) occurs  in a  continuous
path  P  of mate  pairs.    Suppose  L2  is a  distinguished  literal
occurring at an arc below the arc at which L1 occurs.  Suppose a mate
pair (M2 , L2) occurs after the occurrence of (L1 , M1) in P.  Then P
has at least one arc reversal between the occurrence of (L1 , M1) and
the occurrence of (M2 , L2) inclusive.  See figure 3.4. 

	Proof of lemma: By  applying lemma 2 above to  the reverse of
P.  The πreverse of a path (L1 , M1), ..., (Lk , Mk) of mate pairs is
the path (Mk , Lk), ..., (M1 , L1).  Note that the reverse  of a path
is  continuous iff  the path  is.   Also, the  reverse of  a path  is
non-arc reversing iff the path is. 

	Proof of Theorem:  Suppose two non-adjacent  mate pairs of  P
are distinguished clause  repeating.  Let x and y  be mate pairs of P
such that x  occurs earlier  in P  than y,  and such  that the  first
distinguished literal of x is in the same distinguished clause as the
last distinguished  literal of y.  We know  that such mate pairs must
exist.  Suppose x is  (L1 , M1) and y is  (L2 , M2).  Then L1  and M2
are in the same  distinguished clause.  If x and y  occur at the same
pair of arcs, then x and y are themselves arc reversing.  If x occurs
above y, then  P is arc reversing  by the above  lemma.  If x  occurs
below y, then P is arc  reversing by lemma 2 above.  Also, one of the
above three cases must be true since all distinguished literals of  a
distinguished clause are ordered  with respect to one another.   This
completes the proof.